Left Termination of the query pattern
rem_in_3(g, g, a)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).
Queries:
rem(g,g,a).
We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
rem_in: (b,b,f)
sub_in: (b,b,f)
geq_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x4)
U4_GGA(x1, x2, x3) = U4_GGA(x1, x2, x3)
GEQ_IN_GG(x1, x2) = GEQ_IN_GG(x1, x2)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
NOTZERO_IN_G(x1) = NOTZERO_IN_G(x1)
U5_GGA(x1, x2, x3) = U5_GGA(x1, x3)
REM_IN_GGA(x1, x2, x3) = REM_IN_GGA(x1, x2)
SUB_IN_GGA(x1, x2, x3) = SUB_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
U7_GG(x1, x2, x3) = U7_GG(x3)
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
U6_GGA(x1, x2, x3, x4) = U6_GGA(x4)
U4_GGA(x1, x2, x3) = U4_GGA(x1, x2, x3)
GEQ_IN_GG(x1, x2) = GEQ_IN_GG(x1, x2)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
NOTZERO_IN_G(x1) = NOTZERO_IN_G(x1)
U5_GGA(x1, x2, x3) = U5_GGA(x1, x3)
REM_IN_GGA(x1, x2, x3) = REM_IN_GGA(x1, x2)
SUB_IN_GGA(x1, x2, x3) = SUB_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x4)
U7_GG(x1, x2, x3) = U7_GG(x3)
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 3 SCCs with 9 less nodes.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
GEQ_IN_GG(x1, x2) = GEQ_IN_GG(x1, x2)
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
Q DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
SUB_IN_GGA(x1, x2, x3) = SUB_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
SUB_IN_GGA(x1, x2, x3) = SUB_IN_GGA(x1, x2)
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
Q DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(x1, x2, x3) = rem_in_gga(x1, x2)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
U2_gga(x1, x2, x3, x4) = U2_gga(x2, x4)
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U3_gga(x1, x2, x3, x4) = U3_gga(x4)
U4_gga(x1, x2, x3) = U4_gga(x1, x2, x3)
U5_gga(x1, x2, x3) = U5_gga(x1, x3)
geq_in_gg(x1, x2) = geq_in_gg(x1, x2)
U7_gg(x1, x2, x3) = U7_gg(x3)
geq_out_gg(x1, x2) = geq_out_gg
rem_out_gga(x1, x2, x3) = rem_out_gga(x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
REM_IN_GGA(x1, x2, x3) = REM_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
The TRS R consists of the following rules:
notZero_in_g(s(X)) → notZero_out_g(s(X))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
The argument filtering Pi contains the following mapping:
notZero_in_g(x1) = notZero_in_g(x1)
s(x1) = s(x1)
notZero_out_g(x1) = notZero_out_g
sub_in_gga(x1, x2, x3) = sub_in_gga(x1, x2)
U6_gga(x1, x2, x3, x4) = U6_gga(x4)
0 = 0
sub_out_gga(x1, x2, x3) = sub_out_gga(x3)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x2, x4)
REM_IN_GGA(x1, x2, x3) = REM_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y))
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
The TRS R consists of the following rules:
notZero_in_g(s(X)) → notZero_out_g
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y)) at position [2] we obtained the following new rules:
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
The TRS R consists of the following rules:
notZero_in_g(s(X)) → notZero_out_g
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
notZero_in_g(x0)
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
notZero_in_g(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y)) at position [1] we obtained the following new rules:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U1_GGA(x0, 0, notZero_out_g) → U2_GGA(0, sub_out_gga(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U1_GGA(x0, 0, notZero_out_g) → U2_GGA(0, sub_out_gga(x0))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y) we obtained the following new rules:
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule REM_IN_GGA(y0, s(x0)) → U1_GGA(y0, s(x0), notZero_out_g) we obtained the following new rules:
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
By forward instantiating [14] the rule U2_GGA(s(z1), sub_out_gga(x1)) → REM_IN_GGA(x1, s(z1)) we obtained the following new rules:
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
U2_GGA(s(x0), sub_out_gga(s(y_0))) → REM_IN_GGA(s(y_0), s(x0))
The remaining pairs can at least be oriented weakly.
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
| M( sub_in_gga(x1, x2) ) = | | + | | · | x1 | + | | · | x2 |
| M( sub_out_gga(x1) ) = | | + | | · | x1 |
Tuple symbols:
| M( U1_GGA(x1, ..., x3) ) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| M( U2_GGA(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
| M( REM_IN_GGA(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
sub_in_gga(X, 0) → sub_out_gga(X)
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(s(x0), s(x1), notZero_out_g) → U2_GGA(s(x1), U6_gga(sub_in_gga(x0, x1)))
REM_IN_GGA(s(y_0), s(x1)) → U1_GGA(s(y_0), s(x1), notZero_out_g)
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.